A,B:Type.
(x,y:A. decidable((x = y)))
 (u,v:B. decidable((u = v)))
 (x,y:(A + B). decidable((x = y))) 

latex

Definitions	P  Q, decidable(P), x:A. B(x), prop{i:l}, t  T, P  Q, sq_type(T), guard(T), A, False
Lemmas	not wf, decidable wf